T:Type{i}, S:((T){i'}).
(i:. generic{i:l}(T; x.S(i,x)))  generic{i:l}(T; x.(i:. S(i,x))) 

latex

Definitions	Generic{f:T|S(f)}, Type, t  T, , , x:AB(x), f(a), x(s1,s2), x. t(x), x:A. B(x), P  Q, x:A  B(x), Surj(A;B;f), x:A. B(x), ||as||, P & Q, i  j < k, a < b, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, l[i], s = t, type List, l1  l2, t.1, let x,y = A in B(x;y), x.A(x), <a, b>, A c B, {T}, SQType(T), s ~ t, True, T, t.2
Lemmas	pi2 wf, nat sq, pi1 wf, iseg wf, int seg wf, select wf, le wf, length wf1, pair-coding-exists, generic wf, nat wf